es:ES, ff:FIFO, f2f+:F2F+-decls, e:E, sndr, rcvr:ff.C.
[e: rcvr is_req   sndr]  (loc(e) = rcvr  Id) 

latex

Definitions	t  T, P  Q, x:A. B(x), [e: i p j], A c B, P & Q,
Lemmas	event system wf, FIFO wf, F2F+-decls wf, es-E wf, fifoC wf, f2f+Req wf, rcv-it wf, f2f+-property